f || g == x:A. x  dom(f) & x  dom(g)  f(x) = g(x) 

latex

---

clarification:

fpf-compatible(A; a.B(a); eq; f; g)
== x:A. fpf-dom(eq; x; f) & fpf-dom(eq; x; g)  fpf-ap(f; eq; x) = fpf-ap(g; eq; x)  B(x) 

latex

Definitions	x:A. B(x), P  Q, P & Q, b, x  dom(f), f(x)
FDL editor aliases	fpf-compatible